Termination Proof Script
Consider the TRS R consisting of the rewrite rule
1:
f
(
g
(x))
→
f
(
a
(
g
(
g
(
f
(x))),
g
(
f
(x))))
There are 2 dependency pairs:
2:
F
(
g
(x))
→
F
(
a
(
g
(
g
(
f
(x))),
g
(
f
(x))))
3:
F
(
g
(x))
→
F
(x)
The approximated dependency graph contains one SCC: {3}.
Consider the SCC {3}. There are no usable rules. By taking the AF
π
with
π
(
F
) = 1 together with the lexicographic path order with empty precedence, rule 3 is strictly decreasing.
Hence the TRS is terminating.
Tyrolean Termination Tool
(0.00 seconds) --- May 3, 2006